i:Id, ds:x:Id fp Type, x:Id, k:Knd, T:Type, test:(State(ds)T).
((x  dom(ds)))
 ((isrcv(k))  (i = destination(lnk(k))))
 Normal(T)
 Normal(ds)
 es.recognizer(es;i;ds;x;k;T;test) 

latex

Definitions	ES, t  T, x:A. B(x), recognizer(es;i;ds;x;k;T;test), Type, , x. t(x), R ||- es.P(es), P  Q, x:A. B(x), es.P(es), x:AB(x), Normal(ds), Normal(T), lnk(k), destination(l), Id, s = t, isrcv(k), b, x.A(x), a:A fp B(a), Top, IdDeq, x  dom(f), A, , State(ds), Knd, R-base-recognize(i;ds;x;k;T;test)
Lemmas	R-base-recognize-realizes2, fpf wf, Knd wf, decl-state wf, bool wf, not wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, normal-type wf, normal-ds wf, R-base-recognize wf, R-realizes wf, recognizer wf, event system wf